A:Type, eq:EqDecider(A), B:(AType), f,g:fpf(A; a.B(a)), x:A, z:B(x).
fpf-compatible(A; a.B(a); eq; f; g)
 (fpf-cap(fpf-join(eq; f; g); eq; x; z) = fpf-cap(g; eq; x; fpf-cap(f; eq; x; z))  B(x)) 

latex

Definitions	EqDecider(T), fpf-compatible(A; a.B(a); eq; f; g), fpf-cap(f; eq; x; z), P  Q, fpf-join(eq; f; g), if b then t else f fi , Unit, P  Q, P  Q, P  Q, fpf-dom(eq; x; f), fpf(A; a.B(a)), top, x. t(x), fpf-ap(f; eq; x), prop{i:l}, , b, x(s), A, b, x:A. B(x), t  T, False, guard(T)
Lemmas	fpf-ap wf, fpf-join-ap-sq, assert wf, not wf, bnot wf, bool wf, fpf-trivial-subtype-top, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, top wf, fpf-join wf, fpf-join-dom, not functionality wrt iff, deq wf, fpf wf, fpf-compatible wf